Nuprl Lemma : l_index_wf
11,40
postcript
pdf
T
:Type,
dT
:EqDecider(
T
),
L
:(
T
List),
x
:
T
. (
x
L
)
(index(
L
;
x
)
{0..||
L
||
})
latex
Definitions
P
Q
,
P
Q
,
A
c
B
,
i
j
<
k
,
P
&
Q
,
(
x
l
)
,
EqDecider(
T
)
,
index(
L
;
x
)
,
,
A
B
,
A
,
False
,
i
j
,
||
as
||
,
eqof(
d
)
,
l
[
i
]
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
b
,
{
i
..
j
}
Lemmas
int
seg
wf
,
select
wf
,
eqof
wf
,
length
wf1
,
non
neg
length
,
mu-bound
,
deq
wf
,
l
member
wf
,
le
wf
,
assert
wf
,
deq
property
origin
T:Type, dT:EqDecider(T), L:(T List), x:T. (x 
L) 
(index(L;x) {0..||L||
}) T:Type, dT:EqDecider(T), L:(T List), x:T. (x L) (index(L;x) {0..||L||}) 
Q Q
B
j < k l)
B
A
j Qx:A. B(x) T
x:A. B(x)
b}